ALIAS FOL,CLT

.SEND jmc SUBEXP FIX STARTED
TTY GAGged:
21 LETJMC 161  RUNQ-  MAIL    34P  0:00-08  0:00'18-08    21 (FOLCLT)
(Sent to JMC at another, ungagged TTY.)

Exit
↑C
.R FOLISP

Saving input on: BACKUP.TMP

*****SWITCH TO SUBEXP;

You are now using proof: SUBEXP

*****CANCEL 5;

CANCELLED BACK THROUGH 5

*****FETCH SUBEXP.CMD FROM 0;

****
I have used SUBEXP_DEF for making a substitution
I have used SUBEXPF_A for making a substitution
I have used EQV_EQUAL for making a substitution
6 substitutions were made


5 ∀y a.(y subexp a≡y=a)  

****
****
I have used SUBEXP_DEF for making a substitution
I have used SUBEXPF_YY for making a substitution
I have used EQV_OR for making a substitution
I have used EQV_EQUAL for making a substitution
I have used EQV_OR for making a substitution
I have used SUBEXP_DEF for making a substitution
I have used SUBEXP_DEF for making a substitution
10 substitutions were made


6 ∀x yy.(x subexp yy≡(x=yy∨(x subexp car yy∨x subexp cdr yy)))  

****
****
****

7 (∀a y z.(y subexp z⊃(z subexp a⊃y subexp a))∧∀xx.((∀y z.(y subexp z⊃(z subexp car xx⊃y subexp car xx))∧∀y z.(y%
 subexp z⊃(z subexp cdr xx⊃y subexp cdr xx)))⊃∀y z.(y subexp z⊃(z subexp xx⊃y subexp xx))))⊃∀x y z.(y subexp z⊃(%
z subexp x⊃y subexp x))  

****
I have used SUBEXP_A for making a substitution
I have used SUBEXP_A for making a substitution

8 (y subexp z⊃(z subexp a⊃y subexp a))≡(y subexp z⊃(z=a⊃y=a))  

****

9 y subexp z⊃(z subexp a⊃y subexp a)  

****
****

10 ∀a y z.(y subexp z⊃(z subexp a⊃y subexp a))  

****
****

11 ∀y z.(y subexp z⊃(z subexp car xx⊃y subexp car xx))∧∀y z.(y subexp z⊃(z subexp cdr xx⊃y subexp cdr xx))  (11)

****

12 ∀y z.(y subexp z⊃(z subexp car xx⊃y subexp car xx))  (11)

****
****

13 y subexp z⊃(z subexp car xx⊃y subexp car xx)  (11)

****

14 ∀y z.(y subexp z⊃(z subexp cdr xx⊃y subexp cdr xx))  (11)

****
****

15 y subexp z⊃(z subexp cdr xx⊃y subexp cdr xx)  (11)

****
I have used SUBEXP_YY for making a substitution
I have used SUBEXP_YY for making a substitution
2 substitutions were made


16 (y subexp z⊃(z subexp xx⊃y subexp xx))≡(y subexp z⊃((z=xx∨(z subexp car xx∨z subexp cdr xx))⊃(y=xx∨(y subexp %
car xx∨y subexp cdr xx))))  

****

17 y subexp z⊃(z subexp xx⊃y subexp xx)  (11)

****

18 ∀y z.(y subexp z⊃(z subexp xx⊃y subexp xx))  (11)

****

19 (∀y z.(y subexp z⊃(z subexp car xx⊃y subexp car xx))∧∀y z.(y subexp z⊃(z subexp cdr xx⊃y subexp cdr xx)))⊃∀y %
z.(y subexp z⊃(z subexp xx⊃y subexp xx))  

****

20 ∀xx.((∀y z.(y subexp z⊃(z subexp car xx⊃y subexp car xx))∧∀y z.(y subexp z⊃(z subexp cdr xx⊃y subexp cdr xx))%
)⊃∀y z.(y subexp z⊃(z subexp xx⊃y subexp xx)))  

****

21 ∀x y z.(y subexp z⊃(z subexp x⊃y subexp x))  

****
****
I have used SUBEXP_DEF for making a substitution
I have used SUBEXPF_DEF for making a substitution
I have used EQUAL_DEF for making a substitution
I have used ATOM_DEF for making a substitution
I have used NOT_DEF for making a substitution
I have used IF_DEF for making a substitution
I have used IF_X_ATOM for making a substitution
I have used OR_DEF for making a substitution
I have used IF_DEF for making a substitution
I have used AND_DEF for making a substitution
I have used IF_DEF for making a substitution
I have used OR_DEF for making a substitution
I have used IF_DEF for making a substitution
I have used TRUTH1 for making a substitution

22 ∀x.x subexp x  

****
****

23 car yy subexp yy⊃(yy subexp z⊃car yy subexp z)  

****
I have used SUBEXP_YY for making a substitution
I have used SUBEXP_X_X for making a substitution
5 substitutions were made


24 yy subexp z⊃car yy subexp z  

****

25 ∀yy z.(yy subexp z⊃car yy subexp z)  

****
****
****
*****SEND JMC SUBEXP FIX DONE

SEND JMC SUBEXP FIX DONE
↑
This is not a legal command.

*****
*K/F


K/F
↑
This is not a legal command.

*****